import os
import sys
import yaml
import json
import subprocess
from datetime import datetime
from jinja2 import Environment, FileSystemLoader
import argparse
from typing import Dict, Any

class FormalToolkit:
    """形式验证全流程管理工具"""
    
    def __init__(self, config_path: str = "configs/default.yaml"):
        self.config = self._load_config(config_path)
        self.env = Environment(loader=FileSystemLoader("templates"))
        self.results_dir = self._create_results_dir()
        
    def _load_config(self, path: str) -> Dict[str, Any]:
        """加载 YAML 配置文件"""
        with open(path, "r") as f:
            return yaml.safe_load(f)
    
    def _create_results_dir(self) -> str:
        """创建带时间戳的结果目录"""
        timestamp = datetime.now().strftime("%Y%m%d_%H%M%S")
        results_dir = os.path.join("results", f"run_{timestamp}")
        os.makedirs(results_dir, exist_ok=True)
        return results_dir
    
    def generate_sby_config(self) -> str:
        """使用 Jinja2 生成 SBY 配置文件"""
        template = self.env.get_template(self.config["sby_template"])
        sby_content = template.render(**self.config["sby_params"])
        
        sby_path = os.path.join(self.results_dir, "config.sby")
        with open(sby_path, "w") as f:
            f.write(sby_content)

        print(f"[DEBUG] SBY 配置文件已生成: {os.path.abspath(sby_path)}")
        return sby_path
    
    def run_formal(self, sby_path: str) -> Dict[str, Any]:
        """运行 SymbiYosys 并捕获结果"""
        cmd = ["sby", "-f", sby_path, "-d", self.results_dir]
        process = subprocess.Popen(
            cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True
        )
        
        # 实时输出日志到控制台和文件
        log_path = os.path.join(self.results_dir, "sby.log")
        with open(log_path, "w") as log_file:
            for line in process.stdout:
                sys.stdout.write(line)
                log_file.write(line)
        
        process.wait()
        return self._parse_sby_results()
    
    def _parse_sby_results(self) -> Dict[str, Any]:
        """解析 SBY 结果文件"""
        status_path = os.path.join(self.results_dir, "status")
        with open(status_path, "r") as f:
            status_content = f.read()
        
        result = {
            "pass": "PASS" in status_content,
            "log": status_content,
            "traces": [],
            "coverage": self._parse_coverage(),
        }
        
        # 收集反例波形路径
        for engine_dir in os.listdir(self.results_dir):
            if engine_dir.startswith("engine_"):
                trace_path = os.path.join(self.results_dir, engine_dir, "trace.vcd")
                if os.path.exists(trace_path):
                    result["traces"].append(trace_path)
        
        return result
    
    def _parse_coverage(self) -> Dict[str, float]:
        """解析覆盖率结果（需根据工具输出定制）"""
        # 示例：从日志中提取覆盖率数据
        return {"toggle": 95.0, "fsm": 80.0}  # 伪代码
    
    def generate_report(self, result: Dict[str, Any]) -> str:
        """生成 HTML 报告"""
        template = self.env.get_template("report_template.html.j2")
        html_content = template.render(
            config=self.config,
            result=result,
            timestamp=datetime.now().strftime("%Y-%m-%d %H:%M:%S")
        )
        
        report_path = os.path.join(self.results_dir, "report.html")
        with open(report_path, "w") as f:
            f.write(html_content)
        
        return report_path
    
    def open_waveform(self, trace_path: str):
        """调用波形查看器（如 gtkwave）"""
        if sys.platform == "linux":
            subprocess.Popen(["gtkwave", trace_path])
        elif sys.platform == "win32":
            subprocess.Popen(["C:\\Program Files\\gtkwave\\bin\\gtkwave.exe", trace_path])
    
    def interactive_debug(self, result: Dict[str, Any]):
        """交互式调试菜单"""
        if not result["pass"] and result["traces"]:
            choice = input("\n验证失败，选择操作 [V]iew waveform/[R]etry/[I]gnore: ").lower()
            if choice == "v":
                self.open_waveform(result["traces"][0])
            elif choice == "r":
                self.run_formal(self.generate_sby_config())

def main():
    parser = argparse.ArgumentParser(description="形式验证自动化工具")
    parser.add_argument("--config", default="configs/default.yaml", help="配置文件路径")
    parser.add_argument("--report", action="store_true", help="生成HTML报告")
    parser.add_argument("--mode", nargs='+', help="指定验证模式（覆盖配置文件）")
    parser.add_argument("--engines", nargs='+', help="指定验证引擎列表（覆盖配置文件）")
    args = parser.parse_args()
    
    toolkit = FormalToolkit(args.config)
    sby_path = toolkit.generate_sby_config()
    result = toolkit.run_formal(sby_path)
    
    if args.report:
        report_path = toolkit.generate_report(result)
        print(f"报告已生成: file://{os.path.abspath(report_path)}")
    
    if not result["pass"]:
        toolkit.interactive_debug(result)

if __name__ == "__main__":
    main()